$\forall$$T$:Type, $L$:$T$ List, $x$, $y$:$T$. $x$ $<<$ $y$ $\in$ $L$ $\in$ Prop